E:Type{i}, T:(IdIdType{i}), pred?:(E(E+Unit)), info:(E(IdId+(IdLnkE)Id)), when,
after:(x:Ide:ET(loc(e),x)).
SESAxioms{i:l}(E; T; pred?; info; when; after)  Prop{i'} 

latex

Definitions	Id, pred(e), loc(e), SESAxioms{i:l}(E; T; pred?; info; when; after), x:A. B(x), P  Q, destination(l), A & B, Prop, SWellFounded(R(x;y)), x,y. t(x;y), pred!(e;e'), source(l), rcv?(e), link(e), sender(e), e < e', A, b, first(e), P & Q, IdLnk, Unit, P  Q, x:A. B(x), t  T
Lemmas	loc wf, pred wf, Id wf, unit wf, IdLnk wf, first wf, assert wf, not wf, cless wf, sender wf, link wf, rcv? wf, lsrc wf, pred! wf, strongwellfounded wf, ldst wf